A:Type, eq:EqDecider(A), B:(AType), x, y:A, v:B(x), u:B(y).
(x = y  v = u  B(x))  x : v || y : u 

latex

Definitions	x : v, x  dom(f), f(x), false, p  q, eqof(d), b, P  Q, False, P  Q, P & Q, P  Q, f || g, P  Q, Prop, x(s), EqDecider(T), x:A. B(x), t  T
Lemmas	deq wf, deq property, assert of bor, bor wf, assert wf, bfalse wf, eqof wf, subtype rel self